A, B, C:Realizer. A  C  B  C  R-plus(A;B)  C 

latex

Definitions	Rplus-right(x1), Rplus-left(x1), P & Q, Rplus?(x1), Y, Rnone?(x1), A  B, , ff, tt, t  T, if b then t else f fi , let x = a in b(x), R-plus(A;B), P  Q, x:A. B(x), P  Q, Unit, ,
Lemmas	es realizer wf, R-sub wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, Rnone? wf